T:Type, L:T List, i:||L||.
L2:T List, f1:(1||L||), f2:(||L2||||L||).
interleaving_occurence(T;[L[i]];L2;L;f1;f2) & f1(0) = i   

latex

Definitions	P & Q, x:A. B(x), x:A. B(x), ||as||, Dec(P), P  Q, False, A, AB, i  j < k, {i..j}, t  T, Prop, interleaving_occurence(T;L1;L2;L;f1;f2), l[i], True, T, , increasing(f;k), ij, P  Q, hd(l), i<j, ij, {T}, SQType(T), S  T, S  T, P  Q
Lemmas	cons one one, non neg length, member wf, interleaving occurence wf, list extensionality, select wf, nat wf, le wf, decidable lt, int seg wf, length wf1, interleaving split, decidable int equal